lnk:IdLnk, tag:Id, L:Knd List. only events in L send on lnk with tag  Realizer 

latex

Definitions	x:A. B(x), t  T, Realizer, only events in L send on lnk with tag, Prop, x. t(x), x(s)
Lemmas	Id wf, fpf wf, Knd wf, decl-state wf, decl-type wf, IdLnk wf, unit wf